Hint Mode =: Honor all registered modes, enforce = mode in Hint Extern - #22415
Hint Mode =: Honor all registered modes, enforce = mode in Hint Extern#22415Janno wants to merge 3 commits into
=: Honor all registered modes, enforce = mode in Hint Extern#22415Conversation
coqbot-app
Bot
added
the
needs: full CI
|
@coqbot run full ci |
coqbot-app
Bot
removed
the
needs: full CI
|
|
||
| Global Hint Mode C = : typeclass_instances. | ||
|
|
||
| (* Mode [=] gates the extern hint but does not restrict the tactic run by |
There was a problem hiding this comment.
Is this a documented (and intended) feature or more of an implementation artifact? The fact that + guards a Hint Extern, but = does not seems inconsistent.
There was a problem hiding this comment.
Yes, this is explicitly documented in https://rocq-prover.org/doc/v9.3/refman/proofs/automatic-tactics/auto.html#rocq:cmd.Hint-Mode
We could possibly consider a post-hint check that looks at the state of the = arguments and retroactively fails the hint if any evars got instantiated. I do not remember why I didn't consider this for the first implementation.
There was a problem hiding this comment.
What you propose sounds good. In Iris we often use Hint Extern with notypeclasses refine so that we can use the "new" unification (evarconv). It would be awkward if these "instances" have a different behavior regarding modes. So I think the current (documented) behavior is a bug.
Do you want me to make an issue/bug report to track this problem?
There was a problem hiding this comment.
I have optimistically rolled the change into this PR.
coqbot-app
Bot
added
the
needs: full CI
Janno
changed the title
==: Honor all registered modes, enforce = mode in Hint Extern
2 participants
Generated by an LLM. The fix makes sense to me but so did the original code.. :)
Fixes / closes #22413
make doc_gram_rsts.